% $Id$ %
\documentclass[english,a4paper,11pt]{article}
\usepackage{babel}
\usepackage{amsmath,amssymb,amsthm}
% Use utf-8 encoding for foreign characters
\usepackage[utf8]{inputenc}

\usepackage{hyperref}
\usepackage{url}
\usepackage{color}
\usepackage{xspace}
\usepackage{ifpdf}
\usepackage[numbers,sort]{natbib}

\ifpdf
\hypersetup{
    colorlinks,
    urlcolor=blue,
    pdfauthor={Nicholas Kidd}
}
\else
\usepackage{graphicx}
\fi

\theoremstyle{definition}
\newtheorem{codelist}{Code Listing}[section]


\definecolor{bg-gray}{gray}{0.85}
\makeatletter\newenvironment{cmdbox}%
{\begin{lrbox}{\@tempboxa}\begin{minipage}{\textwidth}\small}%
{\normalsize\end{minipage}\end{lrbox}\fcolorbox{black}{bg-gray}{\usebox{\@tempboxa}}}%
\makeatother

\usepackage{listings}
\lstloadlanguages{[GNU]C++}
\lstnewenvironment{cpp}{ \vspace{lex}\noindent
  \lstset{basicstyle=\ttfamily,
  frame=tb,
  columns=fullflexible,
  framexrightmargin=-.2\textwidth,
  prebreak=/,
  breaklines=true
  }
}
{}

% Manual local defs
\def\ONE{\bar{1}}
\def\ZERO{\bar{0}}
\def\hra{\hookrightarrow}
\def\la{\langle}
\def\ra{\rangle}
\def\Rarr{\Rightarrow}
\def\eps{\epsilon}
\def\WALi{\textsf{WALi}\xspace}
\newcommand{\conf}[1]{\langle #1 \rangle}
\newcommand{\Rule}[2]{\conf{#1}\hookrightarrow\conf{#2}}
\newcommand{\longhookrightarrow}{\lhook\joinrel\relbar\joinrel\rightarrow}
\newcommand{\RuleA}[3]{\conf{#1}\;{\buildrel#2\over\longhookrightarrow}\conf{#3}}
\newcommand{\sectref}[1]{\S\ref{Se:#1}}
\newcommand{\figref}[1]{Fig.~\ref{Fi:#1}}
\newcommand{\tableref}[1]{Tab.~\ref{Ta:#1}}

%\title{${\date{\today}}$ WPDS++ User Manual}
\title{\WALi User Manual}
\date{\today}
\author{ Nicholas Kidd \\ { \href{mailto:kidd@cs.wisc.edu}{\nolinkurl{kidd@cs.wisc.edu}}} }

\begin{document}

\maketitle

% Basic introduction
\section{Introduction}
\label{Se:Introduction}
\WALi\footnote{\WALi is short for ``Weighted Automaton Library''} is an open
source library implementation of a Weighted Pushdown System (WPDS). WPDSs have
been shown to be a powerful formalism for performing interprocedural dataflow
analysis \citep{SAS:RSJ:2003,SCP:RSJM:2005,FSTTCS:RLK:2007}. (For a listing of
relevant papers see \url{http://www.cs.wisc.edu/wpis/wpds}.)

\section{Installation}
\label{Se:Installation}
\WALi has been compiled on Linux, Cygwin+Windows/XP and using
Visual Studio 2005. In either case, one must first download the \WALi source
tree. The latest can be found at
\url{http://www.cs.wisc.edu/wpis/wpds/wali/WALi-latest.tar.gz}.
This link will download a gzipped tar file of the \WALi source tree.

\subsection{Linux and Cygwin}
\label{Se:Linux}
\WALi requires a working \href{http://www.python.org}{Python}
installation\footnote{Only Python v2.5 has been fully tested},
the \href{http://www.scons.org}{SCons} build tool, and the common utility
program \verb!curl!. The following commands will download and extract the \WALi
source tree.

\vspace{1em}
\noindent
\begin{cmdbox}
\begin{verbatim}
$ cd <place to untar WALi>
$ curl -O http://www.cs.wisc.edu/wpis/wpds/wali/WALi-latest.tar.gz 
$ tar zxvf WALi-latest.tar.gz
\end{verbatim}
\end{cmdbox}
\vspace{1em}

\noindent  We will use the name \verb!WALiDir! to denote the top level directory of the
\WALi source tree. It is convention to define an environment variable
\verb!$WALiDir! that holds this value.

\vspace{1em}
\noindent
\begin{cmdbox}
\begin{verbatim}
$ cd $WALiDir
$ scons 
\end{verbatim}
\end{cmdbox}
\vspace{1em}

\noindent This will compile and link the \WALi library in the directory
\verb!WALi-1.2/lib!. (For cygwin, a static library is built.) 

The \WALi source tree comes bundled with some examples and addons. These can be
compiled with the commands \verb!scons examples! and \verb!scons addons!,
respectively. The examples include weight domains (\sectref{WeightDomains})
for reachability, kill-gen problems, and affine-relations. The addons includes
C++ code for parsing WPDS queries specified in XML format. The parsing code
makes use of the Apache
\href{http://xerces.apache.org/xerces-c/}{xerces-c} XML parsing
libarary.

After compiling the library, the directory \verb!$WALiDir/lib! should be added
to the environment variable \verb!LD_LIBRARY_PATH! or \verb!PATH! for Linux or
Cygwin, respectively.

\subsection{Visual Studio}
\label{Se:VisualStudio}
Download and extract the \WALi source tree. Underneath the top-level directory of the \WALi
source tree, there is a directory named \verb!Projects!. Underneath the
\verb!Projects! directory there is a file \verb!WALi.vs80.sln!, which is a
Visual Studio solution file containing three projects: \WALi, LiveVar and
Parse. To incorporate \WALi into an existing Visual Studio project, import the
\WALi project (\verb!WALi.vcproj!) if possible, or copy the settings over.
Else, compile the \WALi library using the \WALi solution and set the include and
library directories for an existing Visual Studio project to the appropriate
place.

\section{Interprocedural Control-Flow Graph Encoding}
\label{Se:icfg-encoding}
For performing dataflow analysis, the standard practice is to encode the
program's interprocedural control flow graph as a single state PDS (see
\figref{icfgencoding}). The weights that annotate the rules of the PDS are
dataflow transformers that encode the effect of (abstractly) executing a
program statement associated with the rule.

%% %%%%%%%%%
%% Figure
\begin{figure}[h]
\begin{center}
\begin{tabular}{|l|l|}
  \hline
  Rule & Control flow modeled \\
  \hline \hline
  $\Rule{p,n_1}{p,n_2}$   & Intraprocedural edge $n_1 \to n_2$ \\
  $\Rule{p,n_c}{p,e_f\ r_c}$ & Call to $f$, with entry $e_f$, from $n_c$ that returns to $r_c$ \\
  $\Rule{p,x_f}{p, \eps}$  & Return from $f$ at exit $x_f$ \\
\hline
\end{tabular}
\end{center}
\caption{The encoding of an ICFG's edges as PDS rules.}
\label{Fi:icfgencoding}
\end{figure}
% Implementing a weight domain

\section{Implementing a Weight Domain}
\label{Se:WeightDomains}
\begin{sloppypar}
A \WALi user defines a weight domain $D$ that encodes the desired
abstract domain. $D$ must be a subclass of
the provided abstract class \verb!wali::SemElem!. Inside of \WALi, all
instances of SemElem are reference counted. The reference counting
implementation is defined by the C++ template class \verb!wali::ref_ptr<T>!.
For easier notation, \WALi provides the type definition
\verb!typedef wali::sem_elem_t wali::ref_ptr<wali::SemElem>!.
We next describe each of the methods that must be overridden by the class $D$.
\end{sloppypar}

% One
\subsection{One - $\ONE$}
\begin{verbatim}
sem_elem_t one() const;
\end{verbatim}
\verb!one! returns an instance of the $\ONE$ element.

% Zero
\subsection{Zero - $\ZERO$}
\begin{verbatim}
sem_elem_t zero() const;
\end{verbatim}
\verb!zero! returns an instance of the $\ZERO$ element.

% Combine
\subsection{Combine - $\oplus$}
\begin{verbatim}
sem_elem_t combine( SemElem * se );
\end{verbatim}
\verb!combine! returns a new weight that is the combination of 
\verb!this! and the parameter \verb!se!.

% Extend
\subsection{Extend - $\otimes$}
\begin{verbatim}
sem_elem_t extend( SemElem * se );
\end{verbatim}
\verb!extend! returns a new weight that is 
equal to \verb!this! extended by the parameter
\verb!se! (\verb!this! $\otimes$ \verb!se!). 
\verb!extend! is typically related to functional
composition. Is this regard, \verb!this! $\otimes$ \verb!t! is functionally
equivalent to \verb!t! $\circ$ \verb!this!.

% Equal
\subsection{Equal}
\begin{verbatim}
bool equal( SemElem * se ) const;
\end{verbatim}
\verb!equal! returns true if two weights are equal and
false if not. There is currently no method specifically designed to deal with
partial orders. However, for any two semiring elements 
$\alpha$ and $\beta$, $\alpha$ $\subseteq$ $\beta$ $\Leftrightarrow$$\alpha$ =
($\alpha$ $\oplus$ $\beta$).

% Print
\subsection{Print}
\begin{verbatim}
std::ostream & print( std::ostream & o ) const;
\end{verbatim}
\verb!print! writes a semiring element to the passed in
\verb!std::ostream! parameter. It should return the same
\verb!std::ostream!  when finished.


\section{Examples}
\subsection{Reachability Weight Domain}
The following weight domain implements simple reachability. The weight is
$\ONE$ if it is reachable by the WPDS and $\ZERO$ otherwise. The C++ header
\lstset{language=[GNU]C++,basicstyle=\ttfamily\small}
and source files are distributed with \WALi under the Examples directory.
\begin{codelist}[Weight domain implementing reachability.]
\label{Reach}
\begin{lstlisting}

#include "wali/SemElem.hpp"

using wali::SemElem;
using wali::sem_elem_t;

class Reach : public wali::SemElem
{

  public:

    Reach( bool b ) : isreached(b) {}

    virtual ~Reach() {}

    sem_elem_t one() const { return new Reach(true); }

    sem_elem_t zero() const { return new Reach(false); }

    // zero is the annihilator for extend
    sem_elem_t extend( SemElem* rhs ) {
      Reach* r = static_cast<Reach*>(rhs);
      return new Reach( isreached && r->isreached );
    }
        
    // zero is neutral for combine
    sem_elem_t combine( SemElem* rhs ) {
      Reach* r = static_cast<Reach*>(rhs);
      return new Reach( isreached || r->isreached );
    }
        
    bool equal( SemElem* rhs ) const {
      Reach* r = static_cast<Reach*>(rhs);
      return isreached == r->isreached;
    }

    std::ostream & print( std::ostream & o ) const {
      return (isreached) ? o << "ONE" : o << "ZERO";
    }

  protected:
    bool isreached;

};
\end{lstlisting}
\end{codelist}

Using this weight domain is equivalent to using a Pushdown System without
weights. All user created weights are $\ONE$ and unreachable configurations
(abstractly) have weight $\ZERO$.



\section{Creating a Weighted Pushdown System}
In this section, we show how to translate pseudo code 
following pseudo code is translated
into a WPDS using the \verb!Reach! semiring.
\begin{codelist}[Pseudo Code.]
\label{Fi:PseudoCode}
\begin{lstlisting}

// Pseudo Code //
x = 0
y = 0

fun f()
    n0: <$ f enter node $>
    n1: if( x = 0 )
    n2:     then y := 1
    n3:     else y := 2
    n4: g()
    n5: <$ f exit node $>

fun g()
    n6: <$ g enter node $>
    n7: y := 4
    n8: x := 60
    n9: <$ g exit node $>
\end{lstlisting}
\end{codelist}

\begin{codelist}[\WALi header files]
\label{ExReach}
\begin{lstlisting}

#include "wali/Common.hpp"
#include "wali/wpds/WPDS.hpp"
#include "wali/wfa/WFA.hpp"
#include "Reach.hpp"
\end{lstlisting}
\end{codelist}

First, a WPDS \verb!myWpds! is created. 
\begin{codelist}[Define the WPDS object myWpds.]
\label{myWpds}
\begin{lstlisting}

sem_elem_t reachOne(new Reach(true));
wali::wpds::WPDS myWpds;
\end{lstlisting}
\end{codelist}

Then the ``keys'' for the program locations are defined.
\begin{codelist}[Create Keys for program nodes.]
\label{Keys}
\begin{lstlisting}

wali::Key p = wali::getKey("p");
wali::Key accept = wali::getKey("accept");
wali::Key n[10];
for( int i=0 ; i < 10 ; i++ ) {
  std::stringstream ss;
  ss << "n" << i;
  n[i] = wali::getKey( ss.str() );
}
\end{lstlisting}
\end{codelist}
The state and stack symbols of a WPDS rule have a type \verb!wali::Key!. A key
is a way of identifying a state or stack symbol of the WPDS\@. Each key has a
unique \verb!wali::KeySource! object associated with it. Some common sources
have been defined like \verb!wali::StringSource! and \verb!wali::IntSource!.
User's can define their own key source by subclassing the
\verb!wali::KeySource! class. The function \verb!wali::getKey! is simply a
helpful wrapper for creating a keys from C++ types \verb!std::string! and
\verb!int!. 


Once all the keys have been defined, the rules are added to the
myWpds object.
\begin{codelist}[Add intraprocedural edges for f and g.]
\label{Intra}
\begin{lstlisting}

// f intraprocedural
myWpds.add_rule( p, n[0], p, n[1], reachOne);
myWpds.add_rule( p, n[1], p, n[2], reachOne);
myWpds.add_rule( p, n[1], p, n[3], reachOne);
myWpds.add_rule( p, n[2], p, n[4], reachOne);
myWpds.add_rule( p, n[3], p, n[4], reachOne);

// g intraprocedural
myWpds.add_rule( p, n[6], p, n[7], reachOne);
myWpds.add_rule( p, n[7], p, n[8], reachOne);
myWpds.add_rule( p, n[8], p, n[9], reachOne);
\end{lstlisting}
\end{codelist}

\begin{codelist}[Add interprocedural edges for f and g.]
\label{Intrer}
\begin{lstlisting}

// f calls g
myWpds.add_rule( p, n[4], p, n[6], n[5], reachOne);

// f return
myWpds.add_rule( p, n[5], p, reachOne);

// g return
myWpds.add_rule( p, n[9], p, reachOne);
\end{lstlisting}
\end{codelist}

Then the initialized WPDS is printed to the standard output
channel and marshalled as XML.
\begin{codelist}[Generic output methods.]
\label{Output}
\begin{lstlisting}

// Print the WPDS
myWpds.print( std::cout ) << std::endl;

// Marhasll the WPDS as an XML file
std::ofstream fxml( "myWpds.xml" );
myWpds.marshall( fxml );
fxml.close();
\end{lstlisting}
\end{codelist}


\section{Querying the WPDS}
\label{Se:Query}

\WALi allows for two types of queries, \emph{prestar} and \emph{poststar}. A
query takes as input a WPDS and a weighted finite automaton (WFA). A query
outputs a new annotated WFA\@. WFAs are represented by the class
\verb!wali::wfa::WFA!. Transitions are added to the WFA class using the
\verb!wali::wfa::WFA::addTrans! method. The following sample code computes a
\emph{prestar} and \emph{poststar} reachability query for the pseudo code
(assuming the same objects are created as in the above C++ program).

\begin{codelist}[Prestar query.]
\label{Prestar}
\begin{lstlisting}
    
    wali::wfa::WFA prequery;
    prequery.addTrans( p, n[4], accept, reachOne );
    query.add_initial_state( p );
    query.add_final_state( accept );
    wali::wfa::WFA answer = myWpds.prestar(prequery);
    answer.print( std::cout );
\end{lstlisting}
\end{codelist}

\begin{codelist}[Poststar query.]
\label{Poststar}
\begin{lstlisting}

    wali::wfa::WFA postquery;
    postquery.addTrans( p, n[0], accept, reachOne );
    query.add_initial_state( p );
    query.add_final_state( accept );
    wali::wfa::WFA answer;
    myWpds.poststar(query,answer);
    answer.print( std::cout );
\end{lstlisting}
\end{codelist}


%\input{Querying}

% Appendix A
%\input{differential}

% Appendix B
%\input{ewpds}


% This includes everything in the Bib, remove it if you only want the ones
% actually cited
%\nocite{*}

\bibliographystyle{plainnat}
\bibliography{manual}
\end{document}
